Nuprl Lemma : existse-rcv_wf
0,22
postcript
pdf
es
:ES,
l
:IdLnk,
tg
:Id,
P
:({
e
:E| isrcv(
e
) }
Prop). (
e
=rcv(
l
,
tg
).
P
(
e
))
Prop
latex
Definitions
t
T
,
E
,
b
,
x
:
A
.
B
(
x
)
,
Prop
,
x
(
s
)
,
rcv(
l
,
tg
)
,
kind(
e
)
,
Knd
,
A
&
B
,
x
:
A
.
B
(
x
)
,
P
&
Q
,
e
=rcv(
l
,
tg
).
P
(
e
)
,
ES
,
IdLnk
,
Id
,
isrcv(
e
)
,
True
,
isrcv(
k
)
,
{
T
}
,
P
Q
,
SQType(
T
)
Lemmas
Knd
sq
,
assert
wf
,
es-isrcv
wf
,
Id
wf
,
IdLnk
wf
,
event
system
wf
,
es-E
wf
,
Knd
wf
,
es-kind
wf
,
rcv
wf
origin
es:ES, l:IdLnk, tg:Id, P:({e:E| isrcv(e) }
Prop). (
e=rcv(l,tg). P(e)) 
Prop es:ES, l:IdLnk, tg:Id, P:({e:E| isrcv(e) }Prop). (e=rcv(l,tg). P(e)) Prop T
bx:A. B(x)x:A. B(x)e=rcv(l,tg). P(e)
Q